$\forall$$i$:Id, $l$:IdLnk, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it tg}$:Id, $k$:Knd, $n$, $f$:Top. \\[0ex]msg{-}spec{-}loc{-}decl($k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$;$i$;${\it da}$) \\[0ex]$\Leftrightarrow$ \\[0ex]source($l$) $=$ $i$ \& rcv($l$,${\it tg}$) $\in$ dom(${\it da}$)